A, A':Type.
strong-subtype(A;A')
 (B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'), f, g:a:A fp B(a).
 ((a:A. B(a)  C(a))  f  g  f  g) 

latex

Definitions	x  dom(f), Prop, 2of(t), f(x), {T}, Top, t  T, EqDecider(T), a:A fp B(a), strong-subtype(A;B), A & B, x. t(x), x(s), f  g, x:A. B(x), P  Q, b
Lemmas	fpf-sub wf, strong-subtype-deq-subtype, fpf wf, deq wf, strong-subtype wf, fpf-trivial-subtype-top, fpf-dom-type2, fpf-dom functionality2, fpf-ap wf, top wf, subtype-fpf3, fpf-dom wf, assert wf